package com.Clause;

import java.util.LinkedList;

import Variabilize.Chemin;

public class ClauseBuilder {

	public static Clause newClause(Chemin chemin_depart){

		LinkedList<Chemin> chemins = chemin_depart.getListe();
		
		char debut = chemin_depart.getPlusGrandeVariable(); //derniere lettre inserée
		
		++debut;
		
		Clause clause = new Clause();		
				
		for(int i=0;i<chemins.size();++i){

			Chemin chemin = chemins.get(i);

			Predicat p2 = new Predicat(chemin.getModele2());
			
			if(i==0){ //premier
				Predicat p1 = new Predicat(chemin.getModele());

				for(int x=0;x<chemin.getModele().getArite();++x){
					if(chemin.getLettreModele1(x) != Chemin.VIDE )
						p1.setVariable(x, new Variable(chemin.getLettreModele1(x)));
					else
						p1.setVariable(x, new Variable(debut++));
				}
				OperateurBinaire opbin = OperateurBinaire.newOu();

				if(chemin.getModele().isNegative()){
					OperateurUnaire neg1 = OperateurUnaire.newNot(p1);
					opbin.setElementSuivant(neg1);
				}
				else{
					opbin.setElementSuivant(p1);
				}

				if(chemin.getModele2().isNegative()){
					OperateurUnaire neg2 = OperateurUnaire.newNot(p2);
					opbin.setElementPrecedent(neg2);
				}
				else{
					opbin.setElementPrecedent(p2);
				}

				clause.setRoot(opbin);
			}
			
			else{
				OperateurBinaire opbin = OperateurBinaire.newOu();
				OperateurBinaire root = (OperateurBinaire)clause.getRoot().getElement();
				opbin.setSuivant(root.getPrecedent());

				if(chemin.getModele2().isNegative()){
					OperateurUnaire neg2 = OperateurUnaire.newNot(p2);
					opbin.setElementPrecedent(neg2);
				}
				else{
					opbin.setElementPrecedent(p2);
				}

				root.setElementPrecedent(opbin);
			}
			
			for(int x=0;x<chemin.getModele().getArite();++x){
				if(chemin.getLettreModele2(x) != Chemin.VIDE )
					p2.setVariable(x, new Variable(chemin.getLettreModele2(x)));
				else
					p2.setVariable(x, new Variable(debut++));
			}
		}

		return clause;
	}

}
